\begin{tabbing}
possible{-}world\=\{i:l\}\+
\\[0ex]($D$; $w$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fair{-}fifo\=\{i:l\}\+\+
\\[0ex]($w$)
\-\\[0ex]\& \=($\forall$$i$:Id, $x$:Id. w{-}vartype($w$; $i$; $x$) $\subseteq\rho$ d{-}m($D$; $i$).ds($x$))\+
\\[0ex]\& (\=$\forall$$i$:Id, $a$:w{-}action($w$; $i$).\+
\\[0ex]$\neg$w{-}isnull($w$; $a$) $\Rightarrow$ w{-}valtype($w$; $i$; $a$) $\subseteq\rho$ d{-}m($D$; $i$).da(w{-}kind($w$; $a$)))
\-\\[0ex]\& ($\forall$$l$:IdLnk, ${\it tg}$:Id. ($w$.M($l$,${\it tg}$)) $\subseteq\rho$ d{-}m($D$; source($l$)).da(rcv($l$,${\it tg}$)))
\\[0ex]\& ($\forall$$i$:Id, $x$:Id. d{-}m($D$; $i$).init($x$,w{-}s($w$; $i$; 0; $x$)))
\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$w{-}isnull($w$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ \=(\=islocal(w{-}kind($w$; w{-}a($w$; $i$; $t$)))\+\+
\\[0ex]$\Rightarrow$ \=d{-}m($D$; $i$).pre(act(w{-}kind($w$; w{-}a($w$; $i$; $t$))),\+
\\[0ex]$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$),w{-}val($w$; w{-}a($w$; $i$; $t$))))
\-\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]d{-}m($D$; $i$).ef(w{-}kind($w$; w{-}a($w$; $i$; $t$)),
\\[0ex]$x$,$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$),w{-}val($w$; w{-}a($w$; $i$; $t$)),w{-}s($w$; $i$; ($t$+1); $x$)))
\-\\[0ex]\& (\=$\forall$$l$:IdLnk.\+
\\[0ex]d{-}m($D$; $i$).send(w{-}kind($w$; w{-}a($w$; $i$; $t$));
\\[0ex]$l$;$\lambda$$x$.w{-}s($w$; $i$; $t$; $x$);w{-}val($w$; w{-}a($w$; $i$; $t$));withlnk($l$;w{-}m($w$; $i$; $t$));$i$))
\-\\[0ex]\& (\=$\forall$$x$:Id.\+
\\[0ex]$\neg$d{-}m($D$; $i$).frame(w{-}kind($w$; w{-}a($w$; $i$; $t$)) affects $x$)
\\[0ex]$\Rightarrow$ w{-}s($w$; $i$; $t$; $x$) $=$ w{-}s($w$; $i$; ($t$+1); $x$) $\in$ d{-}m($D$; $i$).ds($x$))
\-\\[0ex]\& (\=$\forall$$l$:IdLnk, ${\it tg}$:Id.\+
\\[0ex]$\neg$d{-}m($D$; $i$).sframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) sends $<$$l$,${\it tg}$$>$)
\\[0ex]$\Rightarrow$ w{-}tagged(${\it tg}$;onlnk($l$;w{-}m($w$; $i$; $t$))) $=$ nil $\in$ w{-}Msg($w$) List))
\-\-\-\\[0ex]\& \=(\=$\forall$$i$:Id, $a$:Id, $t$:$\mathbb{N}$.\+\+
\\[0ex]$\exists$${\it t'}$:$\mathbb{N}$.
\\[0ex]$t$$\leq$${\it t'}$
\\[0ex]\& \=$\neg$w{-}isnull($w$; w{-}a($w$; $i$; ${\it t'}$)) \& w{-}kind($w$; w{-}a($w$; $i$; ${\it t'}$)) $=$ locl($a$) $\in$ Knd\+
\\[0ex]$\vee$ $\neg$$a$ declared in d{-}m($D$; $i$)
\\[0ex]$\vee$ unsolvable d{-}m($D$; $i$).pre($a$,$\lambda$$x$.w{-}s($w$; $i$; ${\it t'}$; $x$)))
\-\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$w{-}isnull($w$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ (\=$\forall$$x$:Id.\+
\\[0ex]$\neg$d{-}m($D$; $i$).aframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) affects $x$)
\\[0ex]$\Rightarrow$ w{-}s($w$; $i$; $t$; $x$) $=$ w{-}s($w$; $i$; ($t$+1); $x$) $\in$ w{-}vartype($w$; $i$; $x$)))
\-\-\\[0ex]\& (\=$\forall$$i$:Id, $x$:Id, $k$:Knd.\+
\\[0ex]$\neg$d{-}m($D$; $i$).rframe($k$ reads $x$) $\Rightarrow$ w{-}machine{-}independent($w$;$i$;$k$;$x$))
\-\\[0ex]\& (\=$\forall$$i$:Id, $t$:$\mathbb{N}$.\+
\\[0ex]$\neg$w{-}isnull($w$; w{-}a($w$; $i$; $t$))
\\[0ex]$\Rightarrow$ (\=$\forall$$l$:IdLnk.\+
\\[0ex]$\neg$d{-}m($D$; $i$).bframe(w{-}kind($w$; w{-}a($w$; $i$; $t$)) sends on $l$)
\\[0ex]$\Rightarrow$ onlnk($l$;w{-}m($w$; $i$; $t$)) $=$ nil $\in$ w{-}Msg($w$) List))
\-\-\-\-\-
\end{tabbing}